perm filename TAKEUC[E78,JMC] blob sn#384954 filedate 1978-09-28 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "MEMO.PUB[LET,JMC]" SOURCE
C00011 00003	.skip 1
C00012 ENDMK
C⊗;
.REQUIRE "MEMO.PUB[LET,JMC]" SOURCE
.at "qF" ⊂"%AF%*"⊃
.turn on "∂"
.CB AN INTERESTING LISP FUNCTION

	Ikuo Takeuchi of the Electrical Communication Laboratory of Nippon
Telephone and Telegraph Co. (Japan's Bell Labs) devised a recursive
function program for testing and comparing LISP systems.  Its virtue is
that it takes a long time to run but doesn't generate large numbers or use
much stack.  The program is

	%2tak(x, y, z) ← qif x ≤ y qthen y
qelse tak(tak(x - 1, y, z), tak(y - 1, z, x), tak(z - 1, x, y))%1,

where the variables may range over the integers (including negative)
or else over real numbers.  The program has
similar properties in the two cases, but some of the proofs seem more
difficult in the real case.
The program has several interesting features.

.item←0
	#. Inspection suggests that the function satisfies the
equation

	%2tak(x + a, y + a, z + a) = tak(x, y, z) + a%1,

whenever the computation terminates, and this follows by subgoal
induction.  Namely, it is true for the non-recursive case, and
assuming it for the referred sets of arguments yields it for the main
set.  A formal proof proceeds as in (McCarthy 1978).

	#. Experiment using LISP indicates first of all that the
value of %2tak(x,_y,_z)%1 is always one of ⊗x, ⊗y or ⊗z.  I don't
see a proof of this fact in isolation.

	#. Like the 91-function, the program computes a simple
non-recursive function.  Using LISP to compute some values of %2tak%1
quickly leads to the guess that it is the same as

	%2tak0(x,y,z) = qif x ≤ y qthen y qelse qif y ≤ z qthen z qelse x%1.

Subsititution shows that ⊗tak0 satisfies the functional equation for
⊗tak, and therefore by the %2minimization schema%1 of (McCarthy 1978),

	%2tak(x, y, z) = tak0(x, y, z)%1

whenever the former terminates.  %2A fortiori%1, this establishes
that %2tak(x,_y,_z)%1 takes one of the variables as value, but maybe
it could be proved separately.

	#. We now want to prove that ⊗tak is total, and we proceed
as follows:

First, we write a %2"derived program" dtak(x,_y,_z)%1 that computes the depth
of recursion involved in computing %2tak(x,_y,_z)%1 using call-by-value.
We have

.begin nofill

	%2dtak(x, y, z) ← qif x ≤ y qthen 0 qelse 1 + max(
%2∂(30)dtak(x_-_1,_y,_z),
∂(30)dtak(y_-_1,_x,_z),
∂(30)dtak(z_-_1,_x,_y),
∂(30)dtak(tak(x_-_1,_y,_z),_tak(y_-_1,_z,_x),_tak(z_-_1,_x,_y)))%1.
.end

Empirical study leads to the conjecture that for integer values of
the variables, ⊗dtak is extensionally equivalent to

	%2dtak0(x,y,z) = dtak00(x - y, z - y)%1,

where

.begin nofill

	%2dtak00(m,n) =∂(19)qif m ≤ 0 qthen 0
%2∂(19)qelse qif n ≥ 2 qthen m + n(n - 1)/2 -1
∂(19)qelse qif n ≥ 0 qthen m
∂(19)qelse qif n = -1 qthen (m + 1)(m + 2)/2 - 1
∂(19)qelse (m - n)(m - n + 1)/2 - m - 1%1.
.end

	We don't bother to verify the conjecture.  Instead we use ⊗dtak0 as
a rank function to prove %2∀i.qF(i)%1 by course-of-values induction where

	%2qF(i) ≡ ∀x y z.(dtak0(x, y, z) = i ⊃ tak(x, y, z) = tak0(x, y, z))%1.

In order to prove this we must show that

.begin nofill

	%2∀x y z.(x > y ⊃
%2∂(13)   dtak0(x_-_1,_y,_z) < dtak0(x,_y,_z)
∂(13)∧_dtak0(y_-_1,_z,_x)_<_dtak0(x,_y,_z)
∂(13)∧_dtak0(z_-_1,_x,_y)_<_dtak0(x,_y,_z)
∂(13)∧_dtak0(tak0(x_-_1,_y,_z),_tak0(y_-_1,_z,_x),_tak0(z_-_1,_x,_y)) <_dtak0(x,_y,_z))%1.
.end

Each of the four inequalities follows from a separate easy case analysis.
Presumably termination could be proved for the non-integer case by
a similar argument with a more complicated formula for ⊗dtak00.  We
leave this as an exercise for the reader.

	#. Like Morris's program

	%2morris(x,y) ← qif x = 0 qthen 1 qelse morris(x - 1, morris(x, y))%1,

⊗tak is more quickly computed by call-by-need.  In fact the number of
function calls appears to be exponential with call-by-value and
quadratic with call-by-need.  The culprit is the third argument
of the outer call, namely %2tak(z_-_1,_x,_y)%1 which is often
unneeded.  Unlike ⊗morris, however, ⊗tak is total.

	A call-by-need version of ⊗tak is given by

	%2ntak(x, y, z) ← vtak <x, y, z>%1

where
.begin nofill

	%2vtak u ← ∂(15)qif numberp u qthen u
%2∂(15)qelse qif qn qd u qthen vtak(qa u) - 1
∂(15)qelse α{vtak qa u, vtak qad uα}[λx y.
∂(30)qif x ≤ y qthen y
∂(30)qelse vtak <∂(39)<x_-_1,_y,_qadd_u>,
∂(39)<y_-_1,_qadd_u,_x>,
∂(39)<qadd_u_-_1,_x,_y>>]%1.
.end

⊗vtak is obtained from ⊗tak in a somewhat ad hoc way.  Since we don't
always compute all arguments of a function we must work with triples
whose elements are either numbers or applications of functions to
arguments.  The only functions that occur are ⊗vtak itself and subtracting
one.  Therefore, a number stands for itself, an application of ⊗vtak is
represented by a triple, and an application of subtracting one is represented
by a list of one element - the inner expression from which one is to be
subtracted.  Perhaps I'm being thick, but it seems to me that call-by-need
requires lists or at least putting symbols on the stack.

	LISP versions of ⊗tak and many of its friends are in the file
TAK.LSP[E78,JMC] at SU-AI.  I thank Don Knuth for suggesting call-by-need.
The external or publication LISP notation is as in (McCarthy and Talcott 1978).
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This version of
TAKEUC[E78,JMC]
translated for printing (by PUB) at {time} on {date}.%1